/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓␈↓ αT␈↓↓alt x ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ x ∨ ␈↓αn␈↓↓ ␈↓αd␈↓↓ x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ ␈↓αa␈↓↓ x . alt ␈↓αdd␈↓↓ x␈↓

␈↓ α∧␈↓(DEFUN ALT (X) (COND
␈↓ α∧␈↓                ((OR (NULL X) (NULL (CDR X))) X)
␈↓ α∧␈↓                (T (CONS (CAR X) (ALT (CDDR X))))
␈↓ α∧␈↓))

␈↓ α∧␈↓␈↓ αTalt[x] = [null[x] ∨ null[cdr[x]] → x; T → cons[car[x]; alt[cddr[x]]]


␈↓ α∧␈↓␈↓ αT␈↓↓alt␈↓ (A B C D E) = (A C E)
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓␈↓ αT␈↓↓mapcar[u,f] ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ ␈↓NIL␈↓↓ ␈↓αelse␈↓↓ f[␈↓αa␈↓↓ u] . mapcar[␈↓αd␈↓↓ u,f]

␈↓ α∧␈↓␈↓ αT␈↓↓maplist[u,f] ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ ␈↓NIL␈↓↓ ␈↓αelse␈↓↓ f[u] . maplist[␈↓αd␈↓↓ u,f]

␈↓ α∧␈↓␈↓ αT␈↓↓diff[exp,var] ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t exp ␈↓αthen␈↓↓ [␈↓αif␈↓↓ exp = var ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ 0]
␈↓ α∧␈↓                ␈↓αelse␈↓ ␈↓αif␈↓ ␈↓αa␈↓ exp = PLUS ␈↓αthen␈↓
␈↓ α∧␈↓                        PLUS␈↓↓ . mapcar[␈↓αd␈↓↓ exp, λx.diff[x,var]]
␈↓ α∧␈↓↓                ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αa␈↓↓ exp = ␈↓TIMES␈↓↓ ␈↓αthen␈↓↓
␈↓ α∧␈↓↓                        ␈↓PLUS␈↓↓.maplist[␈↓αd␈↓↓ exp,λx. ␈↓TIMES␈↓↓.maplist[␈↓αd␈↓↓ exp,
␈↓ α∧␈↓↓λy.␈↓αif␈↓↓ x = y ␈↓αthen␈↓↓ diff[␈↓αa␈↓↓ y,var] ␈↓αelse␈↓↓ ␈↓αa␈↓↓ y]]

␈↓ α∧␈↓↓␈↓ αTdiff[␈↓(TIMES X (PLUS X Y 3)), X] = (PLUS (TIMES 1 (PLUS X Y 3))
␈↓ α∧␈↓↓␈↓(TIMES X (PLUS 1 0 0)))